\begin{tabbing}
$\forall$${\it the\_w}$:World.
\\[0ex]FairFifo
\\[0ex]$\Rightarrow$ val{-}axiom(\=E;${\it the\_w}$.TA;${\it the\_w}$.M;$\lambda$$e$.w{-}info(${\it the\_w}$;$e$);$\lambda$$e$.w{-}pred(${\it the\_w}$;$e$);\+
\\[0ex]$\lambda$$i$,$x$. s($i$;0).$x$;$\lambda$$i$.1of(2of(w{-}machine(${\it the\_w}$;$i$)));$\lambda$$i$.1of(w{-}machine(${\it the\_w}$;$i$));
\\[0ex]$\lambda$$i$.2of(2of(w{-}machine(${\it the\_w}$;$i$)));$\lambda$$e$.val($e$))
\-
\end{tabbing}